enrich gen-secdomain
 , 
       gen-systemstate
 , 
       gen-commands , 
       gen-value , 
       gen-name with
   functions 
      contents : systemstate × name → value;
      comment: Rushby Def. 5;
       
      obs : systemstate × secdomain → systemstate;
      step : systemstate × command → systemstate;
      cdom : command → secdomain;
      comment: Rushby.;
       
      cdom : name → secdomain;
      comment: new by us.;
       
   predicates 
      usedName : name;
      observe : name × secdomain;
      comment: Rushby Def. 5;
       
      alter : name × secdomain;
      comment: Rushby Def. 5;
       
       . ⇒ . : secdomain × secdomain;
      comment: security policy, interference relation;
       
      eqd : systemstate × secdomain × systemstate;
      comment: Rushby Reference Monitor Assumption.;
       
   
   axioms 
      obs-in-domain :  ⊦ usedName(nam) ∧ cdom(nam) ⇒ d → contents(obs(sys, d), nam) = contents(sys, nam);
      used for : s, ls;
       
      obs-other-domain :  ⊦ ¬ (usedName(nam) ∧ cdom(nam) ⇒ d) → contents(obs(sys, d), nam) = null;
      eqd-def :  ⊦ eqd(sys, d, sys0) ↔ (∀ nam. usedName(nam) ∧ cdom(nam) ⇒ d → contents(sys, nam) = contents(sys0, nam));
      extensionality :  ⊦ sys = sys0 ↔ (∀ nam. contents(sys, nam) = contents(sys0, nam));
      RMA-2
      : ⊦ 
          eqd(sys, cdom(co), sys0) ∧ contents(sys, nam) = contents(sys0, nam) ∧ alter(nam, cdom(co)) ∧ usedName(nam)
        → contents(step(sys, co), nam) = contents(step(sys0, co), nam);
      comment: van der Meyden's version.;
       
      RMA-3 :  ⊦ usedName(nam) ∧ contents(step(sys, co), nam) ≠ contents(sys, nam) → alter(nam, cdom(co));
      alter-observe-respects-policy :  ⊦ usedName(nam) ∧ alter(nam, d) ∧ observe(nam, d0) → d ⇒ d0;
      usedName-def :  ⊦ (∃ d. alter(nam, d) ∨ observe(nam, d)) → usedName(nam);
      no-read-up :  ⊦ observe(nam, d) → cdom(nam) ⇒ d;
      comment: this connects observe to the 
                      language based attacker model 
                      (who can see all low variables).;
       
      no-write-down :  ⊦ alter(nam, d) → d ⇒ cdom(nam);
      comment: this follows from alter-observe-respects-policy
                         if we have observe(nam, cdom(nam)) 
                         (this follows from observe-all-names and d ⇒ d);
       
      observe-all-names :  ⊦ cdom(nam) ⇒ d ∧ usedName(nam) → observe(nam, d);
      comment: this is the stronger version of observe, but
                    it is not actually needed. In the language based setting
                    we are talking about a concrete program that has a
                    fixed number of variables/names. We are not interested
                    in variables that do not occur in the program.
                    observe is not equal to readvars(prog) unless we add
                    print(vars, d) at the end.

                    consider low := high, and low is never read in the program.

                    In language based NIF the attacker is outside the system and
                    can observe all low variables at the end.

                    In model based NIF the attacker is part of the system and
                    can only perform (defined) actions. low := high is secure
                    if there is no action that observes low.

                    consider prog: followed by v := v for all v in vars(prog)
                    as actions. Then observe = vars.
                    ;
       
end enrich